YES 1.241 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  (((/=) :: Eq a => a  ->  a  ->  Bool) :: Eq a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  (((/=) :: Eq a => a  ->  a  ->  Bool) :: Eq a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  ((/=) :: Eq a => a  ->  a  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv3600), Succ(xv41000)) → new_primPlusNat(xv3600, xv41000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv3100), Succ(xv4100)) → new_primMulNat(xv3100, Succ(xv4100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv300), Succ(xv400)) → new_primEqNat(xv300, xv400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(ty_Either, eb), ec), bb, cg) → new_esEs0(xv30, xv40, eb, ec)
new_esEs1(Just(xv30), Just(xv40), app(app(app(ty_@3, he), hf), hg)) → new_esEs(xv30, xv40, he, hf, hg)
new_esEs0(Left(xv30), Left(xv40), app(ty_Maybe, fg), fc) → new_esEs1(xv30, xv40, fg)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, bb, app(app(ty_Either, bf), bg)) → new_esEs0(xv32, xv42, bf, bg)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bbh, app(ty_[], bcg)) → new_esEs2(xv31, xv41, bcg)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, bb, app(ty_Maybe, bh)) → new_esEs1(xv32, xv42, bh)
new_esEs0(Right(xv30), Right(xv40), gc, app(app(app(ty_@3, gd), ge), gf)) → new_esEs(xv30, xv40, gd, ge, gf)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(ty_Maybe, bbd)) → new_esEs1(xv30, xv40, bbd)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), app(app(app(ty_@3, bdb), bdc), bdd), bde) → new_esEs(xv30, xv40, bdb, bdc, bdd)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(xv30, xv40, dg, dh, ea)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), app(ty_[], bea), bde) → new_esEs2(xv30, xv40, bea)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), app(ty_Maybe, bdh), bde) → new_esEs1(xv30, xv40, bdh)
new_esEs0(Left(xv30), Left(xv40), app(app(ty_Either, fd), ff), fc) → new_esEs0(xv30, xv40, fd, ff)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, bb, app(app(ty_@2, cb), cc)) → new_esEs3(xv32, xv42, cb, cc)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bbh, app(app(ty_Either, bcd), bce)) → new_esEs0(xv31, xv41, bcd, bce)
new_esEs0(Right(xv30), Right(xv40), gc, app(ty_[], hb)) → new_esEs2(xv30, xv40, hb)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(ty_Maybe, ed), bb, cg) → new_esEs1(xv30, xv40, ed)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bbh, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs(xv31, xv41, bca, bcb, bcc)
new_esEs0(Right(xv30), Right(xv40), gc, app(app(ty_Either, gg), gh)) → new_esEs0(xv30, xv40, gg, gh)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bbh, app(app(ty_@2, bch), bda)) → new_esEs3(xv31, xv41, bch, bda)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, app(ty_Maybe, dc), cg) → new_esEs1(xv31, xv41, dc)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bbh, app(ty_Maybe, bcf)) → new_esEs1(xv31, xv41, bcf)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, app(app(ty_Either, da), db), cg) → new_esEs0(xv31, xv41, da, db)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(ty_Either, bbb), bbc)) → new_esEs0(xv30, xv40, bbb, bbc)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(app(ty_@3, bag), bah), bba)) → new_esEs(xv30, xv40, bag, bah, bba)
new_esEs1(Just(xv30), Just(xv40), app(app(ty_@2, bad), bae)) → new_esEs3(xv30, xv40, bad, bae)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(ty_@2, ef), eg), bb, cg) → new_esEs3(xv30, xv40, ef, eg)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(xv31, xv41, cd, ce, cf)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(ty_@2, bbf), bbg)) → new_esEs3(xv30, xv40, bbf, bbg)
new_esEs2(:(xv30, xv31), :(xv40, xv41), baf) → new_esEs2(xv31, xv41, baf)
new_esEs1(Just(xv30), Just(xv40), app(ty_[], bac)) → new_esEs2(xv30, xv40, bac)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_@2, beb), bec), bde) → new_esEs3(xv30, xv40, beb, bec)
new_esEs0(Right(xv30), Right(xv40), gc, app(app(ty_@2, hc), hd)) → new_esEs3(xv30, xv40, hc, hd)
new_esEs1(Just(xv30), Just(xv40), app(ty_Maybe, bab)) → new_esEs1(xv30, xv40, bab)
new_esEs0(Left(xv30), Left(xv40), app(ty_[], fh), fc) → new_esEs2(xv30, xv40, fh)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(ty_[], bbe)) → new_esEs2(xv30, xv40, bbe)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(ty_[], ee), bb, cg) → new_esEs2(xv30, xv40, ee)
new_esEs0(Right(xv30), Right(xv40), gc, app(ty_Maybe, ha)) → new_esEs1(xv30, xv40, ha)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, app(ty_[], dd), cg) → new_esEs2(xv31, xv41, dd)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, bb, app(ty_[], ca)) → new_esEs2(xv32, xv42, ca)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_Either, bdf), bdg), bde) → new_esEs0(xv30, xv40, bdf, bdg)
new_esEs0(Left(xv30), Left(xv40), app(app(app(ty_@3, eh), fa), fb), fc) → new_esEs(xv30, xv40, eh, fa, fb)
new_esEs0(Left(xv30), Left(xv40), app(app(ty_@2, ga), gb), fc) → new_esEs3(xv30, xv40, ga, gb)
new_esEs1(Just(xv30), Just(xv40), app(app(ty_Either, hh), baa)) → new_esEs0(xv30, xv40, hh, baa)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(xv32, xv42, bc, bd, be)
new_esEs(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), ba, app(app(ty_@2, de), df), cg) → new_esEs3(xv31, xv41, de, df)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: